\documentclass[a4paper,12pt]{report}

\usepackage[francais]{babel}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amsthm}
\usepackage{multicol}

%\renewcommand\labelitemi{\textbullet}

\title{Logique et programmation logique}
\author{Université de Strasbourg}
\date{D'après le cours de M. Julien Narboux}

%\pagestyle{headings}

\begin{document}

\maketitle
\tableofcontents

\chapter{Introduction}
La logique est à la base de toutes les sciences. Les mathématiques en particulier sont fondées exclusivement sur la logique. En 
programmation, la logique est utilisée pour définir la sémantique des langages, pour spécifier, analyser et prouver des 
programmes

Applications :
\begin{itemize}
\item{fondement des maths} 
\item{résultats négatifs (indépendant de l'axiome des parallèles)}
\end{itemize}
En programmation : 
\begin{itemize}
\item{définir la sémantique des langages de programmations}
\item{spécification des programmes}
\item{analyse des programmes}
\item{preuve de programmes}
\item{programmation logique}
\item{ordonnancement}
\item{synthèse et vérification de circuits}
\item{trafic aérien}
\end{itemize}
L'informatique sert en logique pour générer ou vérifier des preuves.

Correspondance Curry-Howard :\\
\begin{tabular}{l|l}
formule & type \\ \hline
preuve & programme \\
vérification d'une & vérification de \\
démonstration & type \\
normalisation de preuves & calcul \\
\end{tabular}

Objetifs du cours :
\begin{itemize}
\item{comprendre la différence entre syntaxe et sémantique}
\item{comprendre la différence entre théorie et méta-théorie}
\item{découvrire la logique proportionelle et le calcul des prédicats}
\end{itemize}

\textbf{Biblio:} David Nour Raffalli : Introduction à la logique, théorie de la démonstration.

%syntaxe : objets que l'on manipule
%sémantique : sens des objets que l'on manipule
\section{Syntaxe vs sémantique}
La \textit{syntaxe} d'un langage formel est l'ensemble des règles désignant si un mot est correct dans le langage.

La \textit{sémantique} d'un langage est une relation entre les formules syntaxiquement correctes et leur signification.

En logique on distinguera : $\Gamma \models P$ et $\Gamma \vdash P$.

\part{Logique propositionnelle}
\chapter{Calcul des propositions}
\section{Syntaxe}

Soit $V$ un ensemble dénombrable de symboles, dits \textit{variables propositionnelles}.
\[V = \{a,b,c,d,e,\dots\}\]
L'ensemble des formules de la logique propositinnelle est définie comme suit : c'est le plus petit ensemble contenant $V$ et clos
 par les opérations binaires : $\wedge, \vee,\Rightarrow$ et par l'opérateur unaire et la constante $\mathsf{T}$

Ordre de priorité : $\neg > \wedge > \vee > \Rightarrow$

Associativité : $\wedge$ et $\vee$ sont associatifs à gauche, $\Rightarrow$ à droite.

En OCaml  :
\begin{verbatim}
type formule =
          Faux
        | Variable of string
        | Nom of formule
        | Et of formule * formule
        | Ou of formule * formule
        | Implique of formule * frmule
\end{verbatim}

Autre exemple : $F = (a\wedge b)\Rightarrow c$
\begin{verbatim}
let f = Implique(Et(Var "a", Var "b"), Var"c");;
\end{verbatim}

\section{Sémantique}
On appelle \textit{interprétation} (ou \textit{valuation}) une application $I$ de $V$ dans $\{0,1\}$. L'application $I$ est étendue
 aux formules de la logique propositionnelle par récurrence sur la structure des formules. On peut citer, à titre d'exemple :

\begin{itemize}
\item[\textbullet]{$I(\neg)=0$}
\item[\textbullet]{$I(\neg A)=1-I(A)$}
\item[\textbullet]{$I(A\wedge B)=I(A)\times I(B)$}
\item[\textbullet]{
$I(A\vee B)=
\left\{
\begin{array}{l l}
1 & \text{si}~ I(A)=1 ~\text{ou}~ I(B)=1 \\
0 & \text{sinon}
\end{array}
\right.$}
\item[\textbullet]{$I(A\Rightarrow B)=1 ~\text{si}~I(A)=0, ~\text{ou}~(I(A)=1~\text{et}~I(B)=1)$}
\end{itemize}
\vspace{10pt}
On dit que $I$ satisfait $A$ si $I(A)=1$, et qu'elle falsifie $A$ si $I(A)=0$

\subsubsection{Table de vérité :} On appelle \textit{table de vérité} la représentation sous forme d'un tableau de la fonction qui associe à chaque interprétation des variables propositionnelles dans $\{0,1\}$. Par exemple :\\

\begin{center}
\begin{tabular}{|c|c||c|}
\hline
$a$ & $b$ & $a\wedge b$ \\ \hline \hline
$0$ & $0$ & $0$ \\ \hline
$0$ & $1$ & $0$ \\ \hline
$1$ & $0$ & $0$ \\ \hline
$1$ & $1$ & $1$ \\ \hline
\end{tabular}
\end{center}

Remarque : il y a $2^{2^n}$ fonctions booléennes à $n$ variables. Par exemple, pour $n=2$ :

\vspace{10pt}
\begin{tabular}{|c|c||c|c|c|c|c|c|c|c|c|c|}
\hline
$A$ & $B$ & $\bot$ & $\wedge$ & $\neg(A\Rightarrow B)$ & $A$ & $\neg(A\Leftarrow B)$ & $B$ & $\neq$ & $\vee$ & $\neg \vee$ & $=$ \\ \hline \hline
$0$ & $0$ & $0$ & $0$ & $0$ & $0$ & $0$ & $0$ & $0$ & $0$ & $1$ & $1$ \\ \hline
$0$ & $1$ & $0$ & $0$ & $0$ & $0$ & $1$ & $1$ & $1$ & $1$ & $0$ & $0$ \\ \hline
$1$ & $0$ & $0$ & $0$ & $1$ & $1$ & $0$ & $0$ & $1$ & $1$ & $0$ & $0$ \\ \hline
$1$ & $1$ & $0$ & $1$ & $0$ & $1$ & $0$ & $1$ & $0$ & $1$ & $0$ & $1$ \\ \hline
\end{tabular}

\vspace{5pt}

\begin{tabular}{|c|c||c|c|c|c|c|c|}\hline
$A$ & $B$ & $\neg B$ & $\Leftarrow$ & $\neg A$ & $\rightarrow$  & $\neg \wedge$ & $\top$\\ \hline
$0$ & $0$ & $1$ & $1$ & $1$ & $1$ & $1$ & $1$ \\ \hline
$0$ & $1$ & $0$ & $0$ & $1$ & $1$ & $1$ & $1$ \\ \hline
$1$ & $0$ & $1$ & $1$ & $0$ & $0$ & $1$ & $1$ \\ \hline
$1$ & $1$ & $0$ & $1$ & $0$ & $1$ & $0$ & $1$ \\ \hline
\end{tabular}

\subsubsection{Satisfiable:}
Une formule $A$ est \textit{satisfiable} s'il existe au moins une interprétation $I$ qui satisfait $A$.

$\Gamma \models A \Leftrightarrow A$ est la conséquence logique de $\Gamma$.

Un ensemble de formules est satisfiable s'il existe une interprétation $I$ qui satisfait toutes les formules de l'ensemble. Par
exemple, $\Gamma_1=\{a,b,a\wedge b\}$ est satisfiable car $I$ telle que $I(a)=1$ et $I(b)=1$ satisfait $\Gamma_1$.

$\Gamma_2=\{a, \neg a\}$ n'est pas satisfiable.

\subsubsection{Insatisfiable:}
Une formule est \textit{insatisfiable} (ou \textit{contradictoire}) si elle n'est pas satisfiable. Une ensemble de formules est insatisfiable s'il n'est
 pas satisfiable.

\subsubsection{Validité:}
Une formule $A$ est \textit{valide} (ou \textit{tautologique}) si toute interprétation satisfait $A$.

\subsubsection{Conséquence:}
Une formule $A$ est \textit{conséquence logique} d'un ensemble de formules $\Gamma$ si toute interprétation qui satisfait $\Gamma$ 
satisfait $A$. Notation : $\Gamma \models A$.

Exemple : \{$p$,$q$\} $\models$ $q$ $\wedge$ $p$

\subsubsection{Méta-théorème de la déduction:}
$\Sigma \models F \Rightarrow G$ si et seulement si $\Sigma, F \models G$. $\Sigma, F$ est une notation pour $\Sigma U \{F\}$.

\begin{proof}
Montrons que si $\Sigma \models F \Rightarrow G$, alors $\Sigma, F \models G$.\\

\textbf{(1)} Supposons que $\Sigma \models F \Rightarrow G$. Montrons que $\Sigma, F \models G$. Montrons que toute interprétation $I$ 
qui satisfait $\Sigma, F$, satisfait $G$.

Par définition, $I$ satisfait $\Sigma$. Donc, comme $\Sigma \models F \Rightarrow G$, on a $I(F\Rightarrow G)=1$. $I$ satisfait
$\Sigma, F$ donc $I(F)=1$. En conclusion, $I(G)=1$.\\

\textbf{(2)} Montrons que si  $\Sigma, F \models G$, alors $\Sigma \models F \Rightarrow G$.

Supposons que $\Sigma, F \models G$. Montrons que $\Sigma \models F \Rightarrow G$.

Montrons que toute interprétation $I$ qui satisfait $\Sigma$ satisfait $F\Rightarrow G$.

Soit $I$ satisfaisant $\Sigma$ : deux cas sont possibles :

Si $I(F)=1$, alors $I$ satisfait $\Sigma, F$, donc $I$ satisfait $G$. On en déduit que $I(F\rightarrow G)=1$.

Si $I(F)=0$, alors $I(F\Rightarrow G)=1$ par définition de l'implication. 
\end{proof}

\subsubsection{\'Equivalence:}
Deux formules sont \textit{équivalentes} (noté $A\equiv B$) si et seulement si ($\{A\}\models B$ et $\{B\}\models A$).

\subsubsection{Quelques équivalences utiles:}
\begin{itemize}
\item[\textbullet] $\models \neg (A \vee B) \Leftrightarrow \neg A \wedge \neg B$
\item[\textbullet] $\models \neg (A \wedge B) \Leftrightarrow \neg A \vee \neg B$
\item[\textbullet] $\neg (A \vee B) \equiv \neg A \wedge \neg B$ (Loi de Morgan)
\item[\textbullet] $\models (A \vee B) \wedge C \Leftrightarrow (A \wedge B) \vee (B \wedge C)$ (Distributivité)
\item[\textbullet] $\models (A \wedge B) \vee C \Leftrightarrow (A \vee B) \wedge (B \vee C)$
\item[\textbullet] $\models (A \Rightarrow B) \Leftrightarrow \neg A \vee B$
\item[\textbullet] $\models \neg \neg A \Leftrightarrow A$
\item[\textbullet] $\models A \wedge \neg A \Leftrightarrow \bot$
\item[\textbullet] $\models A \vee \bot \Leftrightarrow A$
\item[\textbullet] $\models A \wedge \bot \Leftrightarrow \bot$
\item[\textbullet] $\models A \wedge \top \Leftrightarrow A$
\item[\textbullet] $\models A \vee \top \Leftrightarrow \top$
\end{itemize}

\section{Formes canoniques :}
\subsubsection{Forme normale conjonctive:}
On dit que $F$ est sous forme normale conjonctive si $F$ est une conjonction de disjonctions de formules atomiques ou de 
négations de formules atomiques. Pour la logique propositionnelle, les formules atomiques sont les variables. Par exemple :
\[(A \vee \neg B) \wedge (\neg C \vee A) \wedge (D \vee A \vee B)\]
\subsubsection{Mise sous forme normale conjonctive:}
Pour toute formule $F$, i existe une formule $F'$ en forme normale conjonctive telle que $F=F'$.

\begin{proof}
(1)On élimine les $\Leftrightarrow$ en transformant $A \Leftrightarrow B$ en $A\Rightarrow B \wedge B \Rightarrow A$
(2)On élimine des $\Rightarrow$ en transformant $A\Rightarrow B$
\end{proof}

\subsection{Littéral}
\subsubsection{Définitions:}
Un littéral est une variable ou sa négation. Par exemple : \[X; \neg X; A; \neg A\]
Une clause est une disjonction de littéraux. Par exemple : \[A \vee \neg B \vee C\]
Un littéral est dit positif s'il n'a pas de négation, négatif sinon. Par exemple, pour un littéral positif : \[X; Y; Z; T\]
Pour un littéral négatif : \[\neg X;\neg Y;\neg Z;\neg T\]
Une clause de Horn est une clause qui possède au plus un littéral positif. Par exemple : \[P \vee \neg B \vee \neg Q \vee \neg N\]
Les clauses de Horn jouent un rôle important en programmation logique.

\subsection{Méta-théorème:}
La logique propositionnelle est décidable : cela signifie qu'il existe un algorithme qui, étant donné une formule, sait dire si elle est satisfiable ou non.

\subsubsection{Preuve:}
On fait une table de vérité.

\subsection{Substitution:}
Si $F$ et $G$ sont deux formules et $p$ une variable propositionnelle,
on définit par induction la formule $F[p:=G]$.
\begin{itemize}
\item[\textbullet]{$\bot[p:=G]=_{def}\bot$}
\item[\textbullet]{$q[p:=G]=_{def}G~\text{si}~p=q,~q~\text{sinon}$}
\item[\textbullet]{$\neg F[p:=G]=_{def} \neg (F[p:=G]$}
\item[\textbullet]{$F_1 \vee F_2[p:=G]=_{def} F_1[p:=G] \vee F_2[p:=G]$}
\item[\textbullet]{$F_1 \wedge F_2[p:=G]=_{def} F_1[p:=G] \wedge F_2[p:=G]$}
\item[\textbullet]{$F_1 \Rightarrow F_2[p:=G]=_{def} F_1[p:=G] \Rightarrow
F_2[p:=G]$}
\end{itemize}

\subsection{Lemme:}
Soit $I$ une interprétation. Soit $I_0$ l'interprétation définie par
$I_0(p)=I(G)$ et $I_0(q)=I(q)$ pour tout $q$ différent de $p$. Alors :
\[I(F[p:=G])=I_0(F)\]
\begin{proof}
On va procéder par induction (ou récurrence) sur la structure de la formule $F$ :
\vspace{7pt}
\begin{itemize}
\item[\textbullet]{Dans le cas ou $F=\bot$}

\vspace{7pt}
$I(\bot[p:=G])=I(\bot)=0 \\ I_0(\bot)=0$, car il n'y a pas de variable.
\vspace{7pt}
\item[\textbullet]{Dans le cas ou $F=F_1 \wedge F_2$}

\vspace{7pt}
$I(F_1 \wedge F2[p:=G])=I(F_1[p:=G] \wedge F_2[p:=G])$\\
$I(F[p:=G])=1$ ssi $I(F_1[p:=G])=1$ et $I(F_2[p:=G])$\\

Par hypothèse de récurrence, on a :
\begin{enumerate}
\item{$I(F_1[p:=G])=I_0(F_1)$}
\item{$I(F_2[p:=G])=I_0(F_2)$}
\end{enumerate}
D'où $I(F[p:=G])$ ssi $I_0(F_1)=1$ et $I_0(F_2)=1$.
\vspace{7pt}
\item[\textbullet]{Dans le cas ou $F=F_1 \vee F_2$ ou $F=F_1\Rightarrow F_2$ :} même travail que pour $F=F_1\wedge F_2$
\vspace{7pt}
\item[\textbullet]{Dans le cas ou $F=q$ une variable :}
\begin{itemize}
\item{Si $p=q$ : $I(q[p:=G])=I(G)=I_0(q)$}
\item{Si $p!=q$ : $I(q[p:=G])=I(q)=I_0(q)$}
\end{itemize}
\end{itemize}
\end {proof}

\chapter{Systèmes Formels}
\section{Définition}
Un système formel est constitué de trois éléments :\vspace{7pt}
\begin{itemize}
\item[\textbullet]{Un langage, qui est un ensemble de formules}
\item[\textbullet]{Des axiomes, qui forment un sous ensemble de l'ensemble des formules}
\item[\textbullet]{Des règles  de déduction (ou règles d'inférence) ; Ce sont des fonctions qui associent des formules à d'autres formules}
\end{itemize}

\vspace{7pt}\textbf{Remarque :}
Les manipulations effectuées dans un système formel sont purement syntaxiques et n'utilisent aucunement le sens que l'on peut associer aux formules.

\subsection{Notations :}
Il est fréquent de noter les règles de la manière suivante : \[\dfrac{P_1 \quad P_2}{C}\]
où les $P_i$ sont les prémices, et $C$ la conclusion.

\section{Preuve}
\subsection{Définition}
Une preuve (ou déduction) est un arbre dont :
\begin{itemize}
\item[\textbullet]{les feuilles sont des axiomes}
\item[\textbullet]{Les n\oe uds correspondent à des applications, des règles de déduction}
\item[\textbullet]{la racine est la formule prouvée}
\end{itemize}

\section{Théorème}
\subsection{Définition}
Un théorème est une formule dont il existe une preuve. On le note : $\vdash F$, ou $F$ est un théorème.\\

Quelle est la différence entre une preuve mathématique et une preuve formelle ?

On pourrait dire qu'une preuve mathématique est une suite d'arguments pour convaincre un mathématicien de l'existence d'une preuve formelle.

\subsection{Correction}
On dit qu'un système est correct quand tout les théorèmes sont des formules valides. On peut alors écrire que si $\vdash F$, alors $\models F$.

\subsection{Complétude}
On dit qu'un système formel est compelt quand toutes les formules valides sont des théorèmes. On peut alors écrire que si $\models F$, alors $\vdash F$.

\subsection{Cohérence}
On dit qu'un système formel est cohérent s'il existe au moins une formule qui n'est pas un théorème.

\subsection{Consistance}
On dit d'un système formel (comportant une symbole de négation $\neg$) qu'il est consistant s'il n'existe aucune formule $F$ tel que $F$ et $\neg F$ soient des théorèmes.

\subsection{Saturation}
On dit qu'un système formel $S$ est saturé si pour toute formule $F$ qui n'est pas un théorème, le système formel $S'$ obtenu en ajoutant $F$ aux axiomes de $S$ est inconsistant.
\pagebreak
\subsubsection{Méthode pour prouver qu'un système est correct:}
\begin{enumerate}
\item{Prouver que les axiomes sont valides}
\item{Prouver que les règles d'inférence préservent la validité}
\end{enumerate}
\vspace{7pt}

$\dfrac{A_1 \quad A_2 \quad \dots \quad A_n}{B}$ préserve la validité veut dire que si $\models A_1$, $\models A_2$, $\dots$ jusqu'à $\models A_n$, alors $\models B$.

\section{Ensemble récursif}
\subsection{Définition}
On dit qu'un ensemble est récursif (ou décidable) s'il s'agit d'un ensemble dont le test d'appartenance peut être réalisé par un programme informatique qui s'arrête toujours, sans tenir compte des limites de mémoire ou de temps de calcul.

\subsection{Ensemble récursivement énumerable}
Un ensemble récursivement énumérable (ou semi-décidable) est un ensemble qui est le domaine de définition d'une fonction calculable.

\subsection{Théorèmes sur les ensembles récursifs}
\begin{itemize}
\item[\textbullet]{Le complémentaire d'un ensemble décidable est décidable}
\item[\textbullet]{Tout ensemble récursif est récursivement énumérable}
\item[\textbullet]{Un ensemble d'entiers $E$ est récursif ssi $\mathbb{N}_{/E}$ est récursivement énumérable}
\end{itemize}

\subsection{Décidabilité de la déduction}
L'ensemble des déductions est décidable.

\subsection{Enumérabilité des théorèmes}
L'ensemble des théorèmes est semi-décidable.

\part{Formalismes pour la logique}
\chapter{Systèmes à la Hilbert}
Les systèmes à la Hilbert présentent de nombreux schémas d'axiomes, mais peu de règle d'inférence. Dans ces systèmes, on ne manipule pas les formules explicitement.

\section{Logique propositionnelle minimale}
Dans cette logique, on ne dispose que de deux axiomes et d'une seule règle d'inférence. Le langage se retrouve réduit aux variables et à un seul connecteur, $\Rightarrow$.
\end{document}